#include <stdio.h>
#include <stdlib.h>
#define MALLOC(n, type) ((type *) malloc((n)* sizeof(type)))

#define ARG_LEN 16
#define RET_LEN 16
#define BYTE_ARG_COUNT (ARG_LEN * sizeof(unsigned int))
#define BYTE_RET_COUNT (RET_LEN * sizeof(float))
#define NUM 2
#define OFFSET ARG_LEN

 __attribute__((count(ARG_LEN)))
float* Func(unsigned int* arg, int ret_len) __attribute__((returns_count("ret_len")));

float* Func(unsigned int* arg, int ret_len)
{
    for (int i = 0; i < ARG_LEN; i++) {
        arg[i] = 1;
    }
    ret_len = ret_len * sizeof(float);
    char* ret __attribute__((count(ret_len))) = MALLOC (ret_len, char);
    return (float*)ret;     // CHECK-NOT: [[# @LINE ]] warning
}

int main(int argc, char* argv[])
{
    int arg_len = ARG_LEN * NUM;
    if (argc != 1) {
        arg_len = arg_len / NUM;
    }
    unsigned int arg[arg_len];
    float* ret = Func(arg + OFFSET, RET_LEN);     // CHECK-NOT: [[# @LINE ]] warning
    return 0;
}
